Nuprl Lemma : es-msg_wf2
11,40
postcript
pdf
the_es
:ES,
l
:IdLnk,
e
:{
e
:E|
haslnk(
l
;
e
)} . emsg(
e
)
(Msg on
l
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
(Msg on
l
)
,
haslink(
l
;
m
)
,
mlnk(
m
)
,
emsg(
e
)
,
msg(
l
;
t
;
v
)
,
t
.1
,
P
Q
,
A
c
B
,
P
Q
,
P
&
Q
,
,
Msg
,
Msg(
M
)
Lemmas
assert-es-haslnk
,
es-msg
wf
,
es-E
wf
,
assert
wf
,
es-haslnk
wf
,
IdLnk
wf
,
event
system
wf
origin
the_es:ES, l:IdLnk, e:{e:E| 
haslnk(l;e)} . emsg(e) 
(Msg on l) the_es:ES, l:IdLnk, e:{e:E| haslnk(l;e)} . emsg(e) (Msg on l) x:A. B(x) T
Q
B
Q